refactor: incorporate an AxEffects field in SymContext, introduce `SymM` monad for `SymContext` state #180

alexkeizer · 2024-09-23T19:28:38Z

Description:

This turned into a rather big tech-debt removal PR. The primary focus is the removal of the duplication we had between SymContext tracking names of hypotheses, and AxEffects tracking Exprs for those same hypotheses.

Added an effects : AxEffects field to SymContext, which stores the AxEffects for a single (non-aggregated!) step
To make live easier, we introduce a SymM monad, so that we don't have to project out to the effect field every single every time (credits/blame go to @bollu for showing me the MonadStateOf trick).
This allowed us to remove a bunch of fields of SymContext which had duplicates in AxEffects
Also, it allowed us to move reflection of the PC out of explodeSteps and into prepareForNextStep (which was previously called SymContext.next),
Finally, we extract ensureAtMostRunSteps and assertStepTheoremsGenerated functions out of the main body of sym_n

Testing:

What tests have been run? Did make all succeed for your changes? Was
conformance testing successful on an Aarch64 machine? yes

License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

…ext`

…th `getCurrentState` The latter refers to the `currentState` field from `AxEffects`, which stores the same state, but as an Expr

It was unused

…ymContext.next` monadic, and fold-in the reflection of the pc (removing the nextPc argument)

Tactics/Reflect/AxEffects.lean

Tactics/Sym.lean

Tactics/SymContext.lean

Tactics/Common.lean

Tactics/SymContext.lean

Co-authored-by: Shilpi Goel <[email protected]>

…t numbering scheme

alexkeizer · 2024-09-23T21:01:58Z

Hmm, for some reason having a logWarning in the following causes the yellow line to get stuck for a suspicuously long time right at the last line of the def. If I comment out the logWarning, the file build as fast as usual. @bollu any idea what's going on?

EDIT: I thought it might be something off with typeclass synthesis, but putting a #check logWarning (m := SymM) right before doesn't seem to invoke the Yellow Line of Doom (but specifying m := SymM still has the same stuck behaviour, so that's not it, either).

/-- Infer `state_prefix` and `curr_state_number` from the `state` name
as follows: if `state` is `s{i}` for some number `i` and a single character `s`,
then `s` is the prefix and `i` the number,
otherwise ignore `state`, log a warning, and start counting from `s1` -/
def inferStatePrefixAndNumber : SymM Unit := do
  let state ← AxEffects.getCurrentStateName
  let state := state.toString
  let tail := state.toSubstring.drop 1

  if let some currentStateNumber := tail.toNat? then
    modifyThe SymContext ({ · with
      state_prefix := (state.get? 0).getD 's' |>.toString,
      currentStateNumber })
  else
    logWarning ""
    modifyThe SymContext ({ · with
      state_prefix := "s",
      currentStateNumber := 1 })

bollu · 2024-09-24T19:23:58Z

@alexkeizer and I minimized this, and will be sending an issue upstream soon. In the meantime, we also have a workaround so it's all good :)

alexkeizer · 2024-09-24T19:51:03Z

I pushed the workaround, @shigoel this is once more ready for review (and at the top of the priority queue from my side)

shigoel

Thanks!

…ypotheses` functionality into `fromLocalContext` (#181) ### Description: Continues the cleanup started in #180 by getting rid of `h_err?` and `addGoalsForMissingHypotheses`. Note that we remove the ability to add a goal for `CheckSPAlignment`, this option was false by default, and never used ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? yes ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. Co-authored-by: Shilpi Goel <[email protected]>

alexkeizer added 9 commits September 23, 2024 11:14

refactor sym_n implementation to use a state monad for the `SymCont…

73b588e

…ext`

feat: add AxEffects field to SymContext

187d7ce

remove use of evalTactic in stepiTac

b185bb0

get rid of dead code

e3dd1f6

fix: update should expect currentState, not initialState

bc6a373

refactor: remove state field from SymContext, and replace uses wi…

d8d780c

…th `getCurrentState` The latter refers to the `currentState` field from `AxEffects`, which stores the same state, but as an Expr

refactor: remove h_pc field from SymContext

34f3226

It was unused

refactor: rename curr_state_number to currentStateNumber, make `S…

e5becf1

…ymContext.next` monadic, and fold-in the reflection of the pc (removing the nextPc argument)

remove next_state

c208248

alexkeizer requested a review from shigoel as a code owner September 23, 2024 19:28